Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	filter(cons(X,Y),0,M)	→ cons(0,n__filter(activate(Y),M,M))
2:	filter(cons(X,Y),s(N),M)	→ cons(X,n__filter(activate(Y),N,M))
3:	sieve(cons(0,Y))	→ cons(0,n__sieve(activate(Y)))
4:	sieve(cons(s(N),Y))	→ cons(s(N),n__sieve(filter(activate(Y),N,N)))
5:	nats(N)	→ cons(N,n__nats(s(N)))
6:	zprimes	→ sieve(nats(s(s(0))))
7:	filter(X1,X2,X3)	→ n__filter(X1,X2,X3)
8:	sieve(X)	→ n__sieve(X)
9:	nats(X)	→ n__nats(X)
10:	activate(n__filter(X1,X2,X3))	→ filter(X1,X2,X3)
11:	activate(n__sieve(X))	→ sieve(X)
12:	activate(n__nats(X))	→ nats(X)
13:	activate(X)	→ X

There are 10 dependency pairs:

The approximated dependency graph contains one SCC: {14-18,21,22}.

Consider the SCC {14-18,21,22}. The usable rules are {1-5,7-13}. By taking the AF π with π(activate) = π(ACTIVATE) = π(filter) = π(FILTER) = π(n__filter) = π(n__nats) = π(nats) = π(s) = π(SIEVE) = 1 and π(cons) = 2 together with the lexicographic path order with precedence n__sieve ≈ sieve, the rules in {1-5,7-18,21} are weakly decreasing and rule 22 is strictly decreasing. There is one new SCC.
- Consider the SCC {14,15,21}. There are no usable rules. By taking the AF π with π(ACTIVATE) = π(FILTER) = π(n__filter) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 21 is weakly decreasing and the rules in {14,15} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (20.42 seconds) --- May 4, 2006